:- module(chr).
:- export chr_label_with / 2.
:- export chr_resolve / 2.
:- export chr_labeling / 1.
:- export 'CHRdelay' / 3.
:- export chr_labeling / 0.
:- export chr_resolve / 1.
:- export tr_chr / 2.
:- export chr_start_handler / 3.
:- export chr_delayed_goals_handler / 3.
:- export chr_label_with / 1.
:- export chr_get_constraint / 2.
:- export chr_get_constraint / 1.
:- export chr_notrace / 0.
:- export chr_trace / 0.
:- export coca / 1.
:- export 'CHR=' / 2.
:- export 'CHRdelay' / 2.
:- export 'CHRnonvar' / 1.
:- export 'CHRfail' / 0.
:- export 'CHRhead_not_kept' / 1.
:- export 'CHRvar' / 1.
:- export 'CHRgen_num' / 1.
:- export 'CHRcheck_and_mark_applied' / 2.
:- export 'CHRcheck_and_mark_applied' / 5.
:- export 'CHRkeep_heads_checking' / 4.
:- export 'CHRkeep_heads_checking' / 6.
:- export 'CHRalready_in' / 1.
:- export 'CHRkill' / 1.
:- export 'CHRget_delayed_goals' / 2.
:- export chr_macro / 2.
:- export macro(no_delayed_goals / 1, chr : chr_macro / 2, []).
:- export macro(no_global_bindings / 2, chr : chr_macro / 2, []).
:- export macro('CHRhead_not_kept' / 1, chr : tr_chr / 2, [write]).
:- use_module(chr2pl).
:- import last_suspension / 1, new_suspensions / 2 from sepia_kernel.
:- comment(summary, "Constraint Handling Rules Library - obsolescent, use library(ech) instead").
:- comment(author, "Pascal Brisset and Thom Fruehwirth, ECRC").
:- comment(copyright, "Imperial College London and ICL").
:- comment(date, "$Date: 2003/06/05 19:36:58 $").
:- comment(status, deprecated).
:- comment(chr / 1, [summary : "Compile File.chr into a .pl file and load the pl file.\n\n", template : "chr(+File)", desc : html("   Compile File.chr containing constraint handling rules into a .pl file\n   and load the pl file.  Note that even if the file cannot be opened by\n   UNIX (Error 170), a nonempty .pl file will be produced and loaded (with\n   no effect).\n\n<P>\n"), args : ["+File" : "A file name (with extension chr)."], resat : "   No.", fail_if : "   None.\n\n", exceptions : [5 : "File is not an atom or string.", 170 : "UNIX cannot open the file."], eg : "   Success:\n[eclipse]: chr(minmax).\nminmax.chr compiled traceable 106874 bytes in 3.37 seconds\nminmax.pl  compiled traceable 124980 bytes in 1.83 seconds\nyes.\n\n\n\n", see_also : [chr2pl / 1]]).
:- comment(chr2pl / 1, [summary : "Compile File.chr into a .pl file.\n\n", template : "chr2pl(+File)", desc : html("   Compile File.chr containing constraint handling rules into a .pl file.\n   Note that even if the file cannot be opened by UNIX (Error 170), a\n   nonempty .pl file will be produced.\n\n<P>\n"), args : ["+File" : "A file name (with extension chr)."], resat : "   No.", fail_if : "   None.\n\n", exceptions : [5 : "File is not an atom or string.", 170 : "UNIX cannot open the file."], eg : "   Success:\n[eclipse]: chr(minmax).\nminmax.chr compiled traceable 106874 bytes in 3.37 seconds\nyes.\n\n\n\n", see_also : [chr / 1]]).
:- comment(chr_get_constraint / 1, [summary : "Remove a constraint unifying with Constraint from the constraint store.\n\n", template : "chr_get_constraint(?Constraint)", desc : html("   Removes a constraint unifying with Constraint from the constraint store.\n   Note that if the unification with Constraint binds variables occurring\n   also in other constraints in the constraint store, these constraints may\n   be simplified (see last examples).  Thus it is recommended to use either\n   a free variable or a term with variable arguments for Constraint.  Used\n   by advanced constraint handling rules users to manipulate themselves the\n   constraints defined by constraint handling rules.\n\n<P>\n"), args : ["?Constraint" : "A constraint (callable term) defined by constraint handling                rules."], resat : "   Yes.", fail_if : "   Fails if there is no constraint (defined by constraint handling rules)\n   in the constraint store that unifies with Constraint.\n\n", eg : "   Example using the constraint handler for Booleans  bool.chr:\n[eclipse]: chr_get_constraint(C).\nno (more) solution.\n\n[eclipse]: and(X,Y,Z), or(X,Y,Z).\n\nConstraints:\n(1) X_g745 * Y_g777 = Z_g809 % pretty print of and/3 constraint\n(2) X_g745 + Y_g777 = Z_g809 % pretty print of or/3 constraint\n\nyes.\n\n[eclipse]: and(X,Y,Z), or(X,Y,Z), chr_get_constraint(C).\n\nC = X * Y = Z\n\nConstraints:\n(2) X_g765 + Y_g797 = Z_g829\n     More? (;)\n\nC = X + Y = Z\n\nConstraints:\n(1) X_g765 * Y_g797 = Z_g829\n     More? (;)\nno (more) solution.\n\n[eclipse]: and(X,Y,Z), or(X,Y,Z), chr_get_constraint(and(1,A,B)).\n% or/3 - constraint is solved when X is bound to 1\nX = 1\nY = A\nZ = 1\nA = A\nB = 1\n\n[eclipse]: and(X,Y,Z), or(X,Y,Z), chr_get_constraint(and(1,1,0)).\nno (more) solution. % or/3 - constraint fails\n\n[eclipse]: and(X,Y,Z), chr_get_constraint(and(1,1,0)).\n\nX = 1\nY = 1\nZ = 0\n\n\n   The predicate chr_labeling/0 can be defined as:\nlabeling :-\n   chr_get_constraint(C),\n   chr_label_with(C),\n   !,\n   chr_resolve(C),\n   labeling.\n\nlabeling.\n\n\n\n", see_also : [chr_labeling / 0, chr_label_with / 1, chr_resolve / 1, chr_get_constraint / 1, chr_get_constraint / 2]]).
:- comment(chr_get_constraint / 2, [summary : "Remove a constraint in which the variable Variable occurs and which unifies\nwith Constraint from the constraint store.\n\n", template : "chr_get_constraint(Variable,?Constraint)", desc : html("   Removes a constraint in which the variable Variable occurs and which\n   unifies with Constraint from the constraint store.  Note that if the\n   unification with Constraint binds variables occurring also in other\n   constraints in the constraint store, these constraints may be simplified\n   (see last examples).  Thus it is recommended to use either a free\n   variable or a term with variable arguments for Constraint.  Used by\n   advanced constraint handling rules users to manipulate themselves the\n   constraints defined by constraint handling rules.  See also\n   chr_get_constraint/1 for more examples.\n\n<P>\n"), args : ["Variable" : "A free variable.", "?Constraint" : "A constraint (callable term) defined by constraint handling                rules."], resat : "   Yes.", fail_if : "   Fails if Variable is not a free variable or if there is no constraint\n   (defined by constraint handling rules) in the constraint store that\n   unifies with Constraint and in which the variable Variable occurs.\n\n", eg : "   Example using the constraint handler for Booleans  bool.chr:\n[eclipse]: and(X,Y,Z), or(A,B,C), chr_get_constraint(Y,Cstr).\n\nX = X\nZ = Z\nA = A\nB = B\nY = Y\nCstr = X * Y = Z\n\nConstraints:\n(2) A + B = C   % pretty print for or/3 - constraint\n\n     More? (;)\n\nno (more) solution.\n\n\n   The following predicate labeling(+Varlist) labels the variables in the\n   list Varlist:\nlabeling([X|VL]) :-\n   var(X),\n   chr_get_constraint(X,C),\n   chr_label_with(C),\n   !,\n   chr_resolve(C),\n   labeling([X|VL]).\n\nlabeling([X|VL]) :-\n   labeling(VL).\n\nlabeling([]).\n\n\n\n\n", see_also : [chr_labeling / 0, chr_label_with / 1, chr_resolve / 1, chr_get_constraint / 2]]).
:- comment(chr_label_with / 1, [summary : "Checks the label_with declarations of Constraint.\n\n", template : "chr_label_with(+Constraint)", desc : html("   Checks the label_with declarations of Constraint.  Used by advanced\n   constraint handling rules users to write their own labeling procedure\n   for the constraints defined by constraint handling rules.\n\n<P>\n"), args : ["+Constraint" : "A chr constraint."], resat : "   Yes.", fail_if : "   Fails if Constraint is a variable or if Constraint does not have a\n   label_with declaration or if the guard of all unifying label_with\n   declarations fail.\n\n", eg : "   Given the following  label_with declaration (from the example\n   constraint handler in file  time-pc.chr:\nlabel_with path(N, X, Y, L, T, I) if N>1.\n\n[eclipse]: chr_label_with(path(N,X,Y,L,T,I)).\nno (more) solution.\n\n[eclipse]: chr_label_with(path(1,X,Y,L,T,I)).\nno (more) solution.\n\n[eclipse]: chr_label_with(path(2,X,Y,L,T,I)).\nX = X\nY = Y\nL = L\nT = T\nI = I     More? (;)\nno (more) solution.\n\n\n\n\n", see_also : [chr_labeling / 0, chr_resolve / 1, chr_get_constraint / 1, chr_get_constraint / 2]]).
:- comment(chr_labeling / 0, [summary : "Activates the built-in labeling feature for constraint handling rules.\n\n", template : "chr_labeling", desc : html("   The constraint handling rule run-time system provides built-in labeling\n   user-defined constraints.  The built-in labeling is invoked by calling\n   the built-in predicate chr_labeling/0.  Once called, whenever no more\n   constraint handling is possible, the built-in labeling will choose a\n   constraint goal whose label_with declaration is satisfied for labeling.\n   It will introduce choices using the clauses of the constraint.\n\n<P>\n"), args : [], resat : "   Yes.", fail_if : "   None, only on backtracking.\n\n", eg : "\n   A query without and with built-in labeling:\n[eclipse]: minimum(X,Y,Z), maximum(X,Y,W), Z neq W.\n\nX = _g357\nY = _g389\nZ = _g421\nW = _g1227\n\nConstraints:\n(1) minimum(_g357, _g389, _g421)\n(2) _g421 leq _g357\n(3) _g421 leq _g389\n(4) maximum(_g357, _g389, _g1227)\n(5) _g357 leq _g1227\n(7) _g389 leq _g1227\n(10) _g421 lss _g1227\n\nyes.\n\n[eclipse]: minimum(X,Y,Z), maximum(X,Y,W),\n           Z neq W, chr_labeling.\n\nX = Z = _g363\nY = W = _g395\n\nConstraints:\n(10) _g363 lss _g395\n\n     More? (;)\n\nX = W = _g363\nY = Z = _g395\n\nConstraints:\n(17) _g395 lss _g363\nyes.\n\n\n\n", see_also : [chr_label_with / 1, chr_resolve / 1, chr_get_constraint / 1, chr_get_constraint / 2]]).
:- comment(chr_notrace / 0, [summary : "Deactivates the standard or Opium debugger extension for constraint\nhandling rules.\n\n", template : "chr_notrace", desc : html("   The query chr_trace.  deactivates the standard or opium debugger.  In\n   case of the Opium debugger, its window remains until quited.\n\n<P>\n"), args : [], resat : "   No.", fail_if : "   None.\n\n", eg : "   Success:\n[eclipse]: chr_notrace.\nyes.\nDebugger switched off\n\n\n\n", see_also : [chr_opium / 0, chr_trace / 0]]).
:- comment(chr_opium / 0, [summary : "Activates the Opium debugger and shows constraint handling.\n\n", template : "chr_opium", desc : html("   In order to use the Opium debugger, the debug_compile flag must have\n   been on (default) during compilation (chr to pl) and loading of the\n   produced ECLiPSe  code.  The query chr_opium.  opens an Opium window in\n   which the ECLiPSe  code will be traced.  The library chr_opium will be\n   automatically loaded.  Note that the Opium debugger for constraint\n   handling rules works with X graphic interface.  The OPIUM_WINDOW\n   environment variable must thus be set.  An Opium execution can be\n   aborted using the a.  command in Opium.\n\n<P>\n   Both debuggers display user-defined constraints and application of\n   constraint handling rules.  In the Opium debugger, this information\n   corresponds to additional ports of the debugger.  The additional ports\n   are:\n\n<P>\n  * add:  A new constraint is added to the constraint store.\n\n<P>\n  * already_in:  A constraint to be added was already present.\n\n<P>\n   The ports related to application of rules are:\n\n<P>\n  * try_rule:  A rule is tried.\n\n<P>\n  * delay_rule:  The last tried rule cannot fire because the guard did not\n    succeed.\n\n<P>\n  * fire_rule:  The last tried rule fires.\n\n<P>\n   The ports related to labeling are:\n  * try_label:  A label_with declaration is checked.\n\n<P>\n  * delay_label:  The last label_with declaration delays because the guard\n    did not succeed.\n\n<P>\n  * fire_label:  The last tried label_with declaration succeeds, so the\n    clauses of the associated constraint will be used for built-in\n    labeling.\n\n<P>\n   When displayed, each constraint is labeled with a unique integer\n   identifier.  Each rule is labeled with its name as given in the chr\n   source using the @ operator.  If a rule does not have a name, it is\n   displayed together with a unique integer identifier.\n\n<P>\n   See the extension manual chapter on constraint handling rules for more\n   information on the Opium scenario used for debugging.\n\n<P>\n"), args : [], resat : "   No.", fail_if : "   None.\n\n", see_also : [chr_trace / 0, chr_notrace / 0]]).
:- comment(chr_resolve / 1, [summary : "Uses the Prolog clauses to solve a constraint Constraint.\n\n", template : "chr_resolve(+Constraint)", desc : html("   Uses the Prolog clauses to solve a constraint Constraint.  Used by\n   advanced constraint handling rules users to program labeling procedures\n   for the constraints defined by constraint handling rules.\n\n<P>\n"), args : ["+Constraint" : "A constraint (callable term) defined by constraint handling                rules."], resat : "   Yes.", fail_if : "   Fails if there are no Prolog clauses for the constraint or if the bodies\n   of all clauses fail.\n\n", exceptions : [4 : "Constraint is a free variable.", 6 : "Constraint is term which is not a constraint (defined by    constraint handling rules)."], eg : "   Example using the constraint handler for Booleans in file  bool.chr:\n[eclipse]: chr_resolve(X).\ninstantiation fault in is_predicate(_g671 / _g639)\n\n[eclipse]: chr_resolve(and(X,Y)).\nout of range in chr_resolve(and(X,Y))\n\n[eclipse]: chr_resolve(and(X,Y,Z)).\n\nX = 0\nY = Y\nZ = 0     More? (;)\n\nX = 1\nY = Z\nZ = Z\nyes.\n\n[eclipse]: chr_resolve(and(a,b,c)).\nno (more) solution.\n\n\n   The predicate chr_labeling/0 can be defined as:\nlabeling :-\n   chr_get_constraint(C),\n   chr_label_with(C),\n   !,\n   chr_resolve(C),\n   labeling.\n\nlabeling.\n\n\n\n", see_also : [chr_labeling / 0, chr_label_with / 1, chr_get_constraint / 1, chr_get_constraint / 2]]).
:- comment(chr_trace / 0, [summary : "Activates the standard debugger and shows constraint handling.\n\n", template : "chr_trace", desc : html("   In order to use the standard debugger, the debug_compile must have been\n   on (default) during compilation (chr to pl) and loading of the produced\n   ECLiPSe  code.  The query chr_trace.  activates the standard debugger\n   showing more information about the handling of constraints.  In the\n   standard debugger, user-defined constraints are treated as predicates\n   and the information about application of constraint handling rules is\n   displayed without stopping.  The additional information displayed is:\n\n<P>\n  * add:  A new constraint is added to the constraint store.\n\n<P>\n  * already_in:  A constraint to be added was already present.\n\n<P>\n   The ports related to application of rules are:\n\n<P>\n  * try_rule:  A rule is tried.\n\n<P>\n  * delay_rule:  The last tried rule cannot fire because the guard did not\n    succeed.\n\n<P>\n  * fire_rule:  The last tried rule fires.\n\n<P>\n   The ports related to labeling are:\n  * try_label:  A label_with declaration is checked.\n\n<P>\n  * delay_label:  The last label_with declaration delays because the guard\n    did not succeed.\n\n<P>\n  * fire_label:  The last tried label_with declaration succeeds, so the\n    clauses of the associated constraint will be used for built-in\n    labeling.\n\n<P>\n   When displayed, each constraint is labeled with a unique integer\n   identifier.  Each rule is labeled with its name as given in the chr\n   source using the @ operator.  If a rule does not have a name, it is\n   displayed together with a unique integer identifier.\n\n<P>\n"), args : [], resat : "   No.", fail_if : "   None.\n\n", eg : "   Success:\n[eclipse]: chr_trace.\nyes.\nDebugger switched on - creep mode\n[eclipse]: notrace.     % trace only constraints\nDebugger switched off\nyes.\n[eclipse]: minimum(X,Y,Z), maximum(X,Y,Z).\n% trace edited to show only firing rules\n\nADD (1) minimum(X, Y, Z)\nTRY (1) minimum(_g218, _g220, _g222) with propagation\nRULE 'propagation' FIRED\n\n ADD (2) leq(_g665, _g601)\n\n ADD (3) leq(_g665, Var)\n\nADD (4) maximum(_g601, Var, _g665)\nTRY (4) maximum(_g601, Var, _g665) with propagation\nRULE 'propagation' FIRED\n\n ADD (5) leq(_g601, _g665)\n TRY (5) leq(_g601, _g665) (2) leq(_g665, _g601) with antisymmetry\n RULE 'antisymmetry' FIRED\n\nTRY (4) maximum(_g601, Var, _g601) with max_eq\nRULE 'max_eq' FIRED\n\n ADD (6) leq(Var, _g601)\n TRY (3) leq(_g601, Var) (6) leq(Var, _g601) with antisymmetry\n RULE 'antisymmetry' FIRED\n\nTRY (1) minimum(_g601, _g601, _g601) with min_eq\nRULE 'min_eq' FIRED\n\n ADD (7) leq(_g601, _g601)\n TRY (7) leq(_g601, _g601) with reflexivity\n RULE 'reflexivity' FIRED\n\nX = Y = Z = _g558\nyes.\n\n\n\n", see_also : [chr_opium / 0, chr_notrace / 0]]).
:- comment(chr_label_with / 2, hidden).
:- comment(chr_resolve / 2, hidden).
:- comment(chr_labeling / 1, hidden).
:- comment('CHRdelay' / 3, hidden).
